$\forall$$m$, $n$, $k$:$\mathbb{N}$, $f$:($\mathbb{N}$$_{\mbox{\scriptsize $<$$n$}}$$\rightarrow\mathbb{N}$$_{\mbox{\scriptsize $<$$m$}}$), $g$:($\mathbb{N}$$_{\mbox{\scriptsize $<$$k$}}$$\rightarrow\mathbb{N}$$_{\mbox{\scriptsize $<$$m$}}$).
\\[0ex]increasing($f$;$n$)
\\[0ex]$\Rightarrow$ increasing($g$;$k$)
\\[0ex]$\Rightarrow$ ($\forall$$i$:$\mathbb{N}$$_{\mbox{\scriptsize $<$$m$}}$. ($\exists$$j$:$\mathbb{N}$$_{\mbox{\scriptsize $<$$n$}}$. $i$ $=$ $f$($j$) $\in$ $\mathbb{Z}$) $\vee$ ($\exists$$j$:$\mathbb{N}$$_{\mbox{\scriptsize $<$$k$}}$. $i$ $=$ $g$($j$) $\in$ $\mathbb{Z}$))
\\[0ex]$\Rightarrow$ ($\forall$$j_{1}$:$\mathbb{N}$$_{\mbox{\scriptsize $<$$n$}}$, $j_{2}$:$\mathbb{N}$$_{\mbox{\scriptsize $<$$k$}}$. $\neg$$f$($j_{1}$) $=$ $g$($j_{2}$) $\in$ $\mathbb{Z}$)
\\[0ex]$\Rightarrow$ $m$ $=$ $n$+$k$ $\in$ $\mathbb{N}$